Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

Q is empty.


↳ QTRS
  ↳ Overlay + Local Confluence

Q restricted rewrite system:
The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

Q is empty.

The TRS is overlay and locally confluent. By [15] we can switch to innermost.

↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)


Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(rm, n)
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(app'(app'(filter2, app'(f, x)), f), x)
APP'(app'(eq, app'(s, x)), app'(s, y)) → APP'(app'(eq, x), y)
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(app'(add, app'(f, x)), app'(app'(map, f), xs))
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(app, app'(app'(rm, n), x)), y)
APP'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → APP'(app'(add, n), y)
APP'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → APP'(min, app'(app'(add, m), x))
APP'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → APP'(app'(add, n), x)
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(app'(if_rm, app'(app'(eq, n), m)), n)
APP'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → APP'(rm, n)
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(rm, n), x)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(min, app'(app'(add, n), x))
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(app'(filter2, app'(f, x)), f)
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(le, n)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(eq, n)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(filter, f)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(minsort, app'(app'(app, app'(app'(rm, n), x)), y))
APP'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → APP'(app'(add, m), app'(app'(rm, n), x))
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(filter2, app'(f, x))
APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app'(add, n), app'(app'(app, x), y))
APP'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → APP'(app'(rm, n), x)
APP'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → APP'(app'(rm, n), x)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x))))
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(add, app'(f, x))
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app, app'(app'(rm, n), x))
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(app'(map, f), xs)
APP'(app'(app'(app'(filter2, false), f), x), xs) → APP'(filter, f)
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(f, x)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(add, x)
APP'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → APP'(minsort, x)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(app'(filter, f), xs)
APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app'(app, x), y)
APP'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → APP'(app'(minsort, x), app'(app'(add, n), y))
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(if_rm, app'(app'(eq, n), m))
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
APP'(app'(eq, app'(s, x)), app'(s, y)) → APP'(eq, x)
APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app, x)
APP'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → APP'(rm, n)
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(if_min, app'(app'(le, n), m))
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(app'(add, x), app'(app'(filter, f), xs))
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(eq, n)
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
APP'(app'(app'(app'(filter2, false), f), x), xs) → APP'(app'(filter, f), xs)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(app'(eq, n), app'(min, app'(app'(add, n), x)))
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(app'(le, n), m)
APP'(app'(le, app'(s, x)), app'(s, y)) → APP'(app'(le, x), y)
APP'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → APP'(min, app'(app'(add, n), x))
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x))
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(f, x)
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil)
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
APP'(app'(le, app'(s, x)), app'(s, y)) → APP'(le, x)
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(app'(eq, n), m)

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ EdgeDeletionProof

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(rm, n)
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(app'(app'(filter2, app'(f, x)), f), x)
APP'(app'(eq, app'(s, x)), app'(s, y)) → APP'(app'(eq, x), y)
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(app'(add, app'(f, x)), app'(app'(map, f), xs))
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(app, app'(app'(rm, n), x)), y)
APP'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → APP'(app'(add, n), y)
APP'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → APP'(min, app'(app'(add, m), x))
APP'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → APP'(app'(add, n), x)
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(app'(if_rm, app'(app'(eq, n), m)), n)
APP'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → APP'(rm, n)
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(rm, n), x)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(min, app'(app'(add, n), x))
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(app'(filter2, app'(f, x)), f)
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(le, n)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(eq, n)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(filter, f)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(minsort, app'(app'(app, app'(app'(rm, n), x)), y))
APP'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → APP'(app'(add, m), app'(app'(rm, n), x))
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(filter2, app'(f, x))
APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app'(add, n), app'(app'(app, x), y))
APP'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → APP'(app'(rm, n), x)
APP'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → APP'(app'(rm, n), x)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x))))
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(add, app'(f, x))
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app, app'(app'(rm, n), x))
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(app'(map, f), xs)
APP'(app'(app'(app'(filter2, false), f), x), xs) → APP'(filter, f)
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(f, x)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(add, x)
APP'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → APP'(minsort, x)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(app'(filter, f), xs)
APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app'(app, x), y)
APP'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → APP'(app'(minsort, x), app'(app'(add, n), y))
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(if_rm, app'(app'(eq, n), m))
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
APP'(app'(eq, app'(s, x)), app'(s, y)) → APP'(eq, x)
APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app, x)
APP'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → APP'(rm, n)
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(if_min, app'(app'(le, n), m))
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(app'(add, x), app'(app'(filter, f), xs))
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(eq, n)
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
APP'(app'(app'(app'(filter2, false), f), x), xs) → APP'(app'(filter, f), xs)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(app'(eq, n), app'(min, app'(app'(add, n), x)))
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(app'(le, n), m)
APP'(app'(le, app'(s, x)), app'(s, y)) → APP'(app'(le, x), y)
APP'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → APP'(min, app'(app'(add, n), x))
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x))
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(f, x)
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil)
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
APP'(app'(le, app'(s, x)), app'(s, y)) → APP'(le, x)
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(app'(eq, n), m)

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.
We deleted some edges using various graph approximations

↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ EdgeDeletionProof
            ↳ QDP
              ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(rm, n)
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(app'(app'(filter2, app'(f, x)), f), x)
APP'(app'(eq, app'(s, x)), app'(s, y)) → APP'(app'(eq, x), y)
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(app'(add, app'(f, x)), app'(app'(map, f), xs))
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(app, app'(app'(rm, n), x)), y)
APP'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → APP'(app'(add, n), y)
APP'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → APP'(min, app'(app'(add, m), x))
APP'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → APP'(app'(add, n), x)
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(app'(if_rm, app'(app'(eq, n), m)), n)
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(rm, n), x)
APP'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → APP'(rm, n)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(min, app'(app'(add, n), x))
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(app'(filter2, app'(f, x)), f)
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(le, n)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(eq, n)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(filter, f)
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(minsort, app'(app'(app, app'(app'(rm, n), x)), y))
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
APP'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → APP'(app'(add, m), app'(app'(rm, n), x))
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(filter2, app'(f, x))
APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app'(add, n), app'(app'(app, x), y))
APP'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → APP'(app'(rm, n), x)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x))))
APP'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → APP'(app'(rm, n), x)
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(add, app'(f, x))
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app, app'(app'(rm, n), x))
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(app'(map, f), xs)
APP'(app'(app'(app'(filter2, false), f), x), xs) → APP'(filter, f)
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(f, x)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(add, x)
APP'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → APP'(minsort, x)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(app'(filter, f), xs)
APP'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → APP'(app'(minsort, x), app'(app'(add, n), y))
APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app'(app, x), y)
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(if_rm, app'(app'(eq, n), m))
APP'(app'(eq, app'(s, x)), app'(s, y)) → APP'(eq, x)
APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app, x)
APP'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → APP'(rm, n)
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(if_min, app'(app'(le, n), m))
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(eq, n)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(app'(add, x), app'(app'(filter, f), xs))
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(app'(eq, n), app'(min, app'(app'(add, n), x)))
APP'(app'(app'(app'(filter2, false), f), x), xs) → APP'(app'(filter, f), xs)
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(app'(le, n), m)
APP'(app'(le, app'(s, x)), app'(s, y)) → APP'(app'(le, x), y)
APP'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → APP'(min, app'(app'(add, n), x))
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x))
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(f, x)
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil)
APP'(app'(le, app'(s, x)), app'(s, y)) → APP'(le, x)
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(app'(eq, n), m)

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 7 SCCs with 37 less nodes.

↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ EdgeDeletionProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                    ↳ QDPOrderProof
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app'(app, x), y)

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13]. Here, we combined the reduction pair processor with the A-transformation [14] which results in the following intermediate Q-DP Problem.
Q DP problem:
The TRS P consists of the following rules:

APP(add(n, x), y) → APP(x, y)

R is empty.
The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)
map(x0, nil)
map(x0, add(x1, x2))
filter(x0, nil)
filter(x0, add(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.


The following pairs can be oriented strictly and are deleted.


APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app'(app, x), y)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
APP(x1, x2)  =  x1
add(x1, x2)  =  add(x1, x2)

Lexicographic Path Order [19].
Precedence:
trivial

The following usable rules [14] were oriented: none



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ EdgeDeletionProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                    ↳ QDPOrderProof
                      ↳ QDP
                        ↳ PisEmptyProof
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ EdgeDeletionProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                    ↳ QDPOrderProof
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(le, app'(s, x)), app'(s, y)) → APP'(app'(le, x), y)

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13]. Here, we combined the reduction pair processor with the A-transformation [14] which results in the following intermediate Q-DP Problem.
Q DP problem:
The TRS P consists of the following rules:

LE(s(x), s(y)) → LE(x, y)

R is empty.
The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)
map(x0, nil)
map(x0, add(x1, x2))
filter(x0, nil)
filter(x0, add(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.


The following pairs can be oriented strictly and are deleted.


APP'(app'(le, app'(s, x)), app'(s, y)) → APP'(app'(le, x), y)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
LE(x1, x2)  =  LE(x2)
s(x1)  =  s(x1)

Lexicographic Path Order [19].
Precedence:
s1 > LE1

The following usable rules [14] were oriented: none



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ EdgeDeletionProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                    ↳ QDPOrderProof
                      ↳ QDP
                        ↳ PisEmptyProof
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ EdgeDeletionProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ QDPOrderProof
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → APP'(min, app'(app'(add, n), x))
APP'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → APP'(min, app'(app'(add, m), x))
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13]. Here, we combined the reduction pair processor with the A-transformation [14] which results in the following intermediate Q-DP Problem.
Q DP problem:
The TRS P consists of the following rules:

MIN(add(n, add(m, x))) → IF_MIN(le(n, m), add(n, add(m, x)))
IF_MIN(false, add(n, add(m, x))) → MIN(add(m, x))
IF_MIN(true, add(n, add(m, x))) → MIN(add(n, x))

The TRS R consists of the following rules:

le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)
map(x0, nil)
map(x0, add(x1, x2))
filter(x0, nil)
filter(x0, add(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.


The following pairs can be oriented strictly and are deleted.


APP'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → APP'(min, app'(app'(add, n), x))
APP'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → APP'(min, app'(app'(add, m), x))
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
MIN(x1)  =  MIN(x1)
add(x1, x2)  =  add(x2)
IF_MIN(x1, x2)  =  IF_MIN(x1, x2)
le(x1, x2)  =  le
false  =  false
true  =  true
0  =  0
s(x1)  =  s

Lexicographic Path Order [19].
Precedence:
add1 > MIN1 > IFMIN2
add1 > MIN1 > le > false
add1 > MIN1 > le > true
s > false

The following usable rules [14] were oriented:

app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(le, app'(s, x)), 0) → false



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ EdgeDeletionProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ QDPOrderProof
                      ↳ QDP
                        ↳ PisEmptyProof
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ EdgeDeletionProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ QDPOrderProof
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(eq, app'(s, x)), app'(s, y)) → APP'(app'(eq, x), y)

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13]. Here, we combined the reduction pair processor with the A-transformation [14] which results in the following intermediate Q-DP Problem.
Q DP problem:
The TRS P consists of the following rules:

EQ(s(x), s(y)) → EQ(x, y)

R is empty.
The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)
map(x0, nil)
map(x0, add(x1, x2))
filter(x0, nil)
filter(x0, add(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.


The following pairs can be oriented strictly and are deleted.


APP'(app'(eq, app'(s, x)), app'(s, y)) → APP'(app'(eq, x), y)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
EQ(x1, x2)  =  EQ(x2)
s(x1)  =  s(x1)

Lexicographic Path Order [19].
Precedence:
s1 > EQ1

The following usable rules [14] were oriented: none



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ EdgeDeletionProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ QDPOrderProof
                      ↳ QDP
                        ↳ PisEmptyProof
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ EdgeDeletionProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ QDPOrderProof
                  ↳ QDP
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → APP'(app'(rm, n), x)
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
APP'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → APP'(app'(rm, n), x)

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13]. Here, we combined the reduction pair processor with the A-transformation [14] which results in the following intermediate Q-DP Problem.
Q DP problem:
The TRS P consists of the following rules:

RM(n, add(m, x)) → IF_RM(eq(n, m), n, add(m, x))
IF_RM(true, n, add(m, x)) → RM(n, x)
IF_RM(false, n, add(m, x)) → RM(n, x)

The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)
map(x0, nil)
map(x0, add(x1, x2))
filter(x0, nil)
filter(x0, add(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.


The following pairs can be oriented strictly and are deleted.


APP'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → APP'(app'(rm, n), x)
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
APP'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → APP'(app'(rm, n), x)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
RM(x1, x2)  =  RM(x2)
add(x1, x2)  =  add(x2)
IF_RM(x1, x2, x3)  =  IF_RM(x3)
eq(x1, x2)  =  eq
true  =  true
false  =  false
0  =  0
s(x1)  =  x1

Lexicographic Path Order [19].
Precedence:
add1 > RM1 > IFRM1
eq > true > RM1 > IFRM1
eq > false > IFRM1
0 > false > IFRM1

The following usable rules [14] were oriented: none



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ EdgeDeletionProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ QDPOrderProof
                      ↳ QDP
                        ↳ PisEmptyProof
                  ↳ QDP
                  ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ EdgeDeletionProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
APP'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → APP'(app'(minsort, x), app'(app'(add, n), y))
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil)

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ EdgeDeletionProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(app'(map, f), xs)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(app'(filter, f), xs)
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(f, x)
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(f, x)
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
APP'(app'(app'(app'(filter2, false), f), x), xs) → APP'(app'(filter, f), xs)

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be oriented strictly and are deleted.


APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(app'(map, f), xs)
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(f, x)
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(f, x)
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
The remaining pairs can at least be oriented weakly.

APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(app'(filter, f), xs)
APP'(app'(app'(app'(filter2, false), f), x), xs) → APP'(app'(filter, f), xs)
Used ordering: Combined order from the following AFS and order.
APP'(x1, x2)  =  APP'(x2)
app'(x1, x2)  =  app'(x1, x2)
map  =  map
add  =  add
filter2  =  filter2
true  =  true
filter  =  filter
false  =  false
le  =  le
0  =  0
nil  =  nil
minsort  =  minsort
eq  =  eq
rm  =  rm
app  =  app
s  =  s
if_rm  =  if_rm
min  =  min
if_minsort  =  if_minsort
if_min  =  if_min

Lexicographic Path Order [19].
Precedence:
APP'1 > app'2
map > app'2
filter2 > app'2
true > app'2
filter > app'2
false > app'2
le > app'2
minsort > app'2
rm > add > ifrm > app'2
rm > eq > app'2
app > app'2
s > app'2
min > app'2
ifminsort > app'2
ifmin > app'2

The following usable rules [14] were oriented: none



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ EdgeDeletionProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ QDPOrderProof
                      ↳ QDP
                        ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(app'(filter, f), xs)
APP'(app'(app'(app'(filter2, false), f), x), xs) → APP'(app'(filter, f), xs)

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 0 SCCs with 2 less nodes.